/**                   GNU GENERAL PUBLIC LICENSE
 *                       Version 3, 29 June 2007
 *
 * Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>
 * Everyone is permitted to copy and distribute verbatim copies
 * of this license document, but changing it is not allowed.
 * See License.txt file that comes with this distribution
 *
 *
 * Author: Vitaly German <vitaly.german@gmail.com>, (C) 2006-2008
 * 
 **/
#ifndef PROBLEM_H
#define PROBLEM_H
#include "rlinear_gen.h"


#include <boost/shared_ptr.hpp>
#include <boost/bind.hpp>

#include "variable.h"

#include <vector>
#include <cstdlib> //exit()
#include <list>

#include "lib/bimap.hpp"  /// bidirectional map

#ifdef USE_RATIONAL
    #include "boost/rational.hpp"
    #define MATIRIX_TYPE_IS_NOT_FUNDAMENTAL
    typedef boost::rational<long long> coef_t;
#else
    typedef double coef_t;
#endif	    


#include "smatrix/smatrix2.hpp"
#include "equalities/eliminate_eq.hpp"

// #define DEBUG_PROBLEM
/**
 * Represents a system of the inequalities and the equalities
 * More real that matrix will be taken as core
 
   @author Vitaly German
 **/
//using namespace smatrix;
using namespace smatrix2;
using namespace std;

namespace rfm_solver {
// Some keys
// May be move to separate class

const size_t maxINEQs=5000;
const size_t INT_PROBLEM_SIZE = 1000*1000*50; // 50M
const bool EnableVaribleChoise = true;

typedef std::list<size_t> PIntList;
typedef boost::shared_ptr<PIntList> PIntList_aptr;
typedef std::pair<int,int> Pair;


typedef std::pair<int, coef_t> Int2Coef;

typedef std::vector<Int2Coef> VecInt2Coef;

typedef std::vector<coef_t> Coefs;


typedef smatrix2::sparse_matrix2 <coef_t>   SparseMatrix;
typedef SparseMatrix * SparseMatrix_ptr;
typedef boost::shared_ptr<SparseMatrix>  SparseMatrix_aptr;

typedef std::vector<Constraint_Property> ConstraintsType;
typedef boost::shared_ptr<ConstraintsType> ConstraintsType_aptr;

typedef SparseMatrix::vector_mx Constants;
typedef boost::shared_ptr<Constants> Constants_aptr;

typedef boost::shared_ptr<Coefs>  Coefs_aptr;

typedef std::vector<int> Ints ;
typedef std::vector<size_t> PInts ;
typedef boost::shared_ptr<Ints> Ints_aptr;

class NewMatrixBuilder;
class Marker;


struct Constraint_Property {
    Constraint_Type type;
    Constraint_Color color;
    Constraint_Property(Constraint_Type t, Constraint_Color c):type(t),color(c) {}
    Constraint_Property() {}
   
    inline bool operator == ( const Constraint_Property & other) const {
        return (type==other.type ? color==other.color : false);
    }
    inline bool operator < ( const Constraint_Property & other) const {
        return (type < other.type || color < other.color);
    }
    inline bool operator != ( const Constraint_Property & other) const {
        return ! (*this == other);
    }
    friend ostream & operator<< ( ostream & os, const Constraint_Property & c) { // unfortunately cannot be moved to cpp. maybe because used by templates
        os<<"(";
        switch (c.type) {
        case TREM:
            os<<" DELETED ";
            break;
        case TGEQ:
            os<<" >= ";
            break;
        case TGE:
            os<<" > ";
            break;
        case TEQ:
            os<<" = ";
            break;
        case TINCONS:
           os<<" INCONS ";
            break;
        default:
            assert( 0 && "Constraint_Property::type unexpected type");
        }

        if (c.color == BLACK) {
            os<<" BLACK ";
        } else if (c.color == RED) {
            os<<" RED ";
        } else {
            assert(0&&"Constraint_Property::color was not set");
        };
        os<<")";
        return os;
    }

};


template <typename T>
ostream & operator<< ( ostream & out, const list <T> & m ){
    out<< "["<<m.size()<<"]";
    out<<":(";
    for(typename list <T> ::const_iterator it =  m.begin(); it!= m.end(); it++){
    	if (it != m.begin()) out<<", ";
        out<<*it;
    }
    out<<")"<<flush;
    return out;
};

/**
 * This struct is returned after elimintion of paralel facets
 * by Problem::eliminate_p_redundant.
 **/

struct RedundantPOut{
    bool consistent; /// true if consistent
    size_t nremoved; /// number of removed facets
    bool eq_created; /// true if new equalities were intronduced
    Conjunct_aptr in_gist; /// if called with enabled gist parameter all RED inconsistent will be putted here
    RedundantPOut(bool cons, size_t nrem, bool eq_c = false, Conjunct_aptr in_g = Conjunct_aptr())
        :consistent(cons), nremoved(nrem), eq_created(eq_c), in_gist(in_g){}
    /// update current results with other one
    void update(const RedundantPOut & o);
};
class EqMapingData{

public:
	typedef std::vector<size_t> VarMap;
	typedef std::list<size_t> EqMap;
	typedef  boost::shared_ptr<VarMap> VarMap_aptr;
	typedef  boost::shared_ptr<EqMap> EqMap_aptr;
	EqMapingData(
		const VarMap_aptr & var_map1,
		const EqMap_aptr &eq_map1
		):var_map_(var_map1), eq_map_(eq_map1)  {}
	EqMapingData(){}
	void var_map(VarMap_aptr & vm) {var_map_ = vm;}
	void eq_map(EqMap_aptr eq_map) {eq_map_ = eq_map;}
	VarMap_aptr var_map() const { return var_map_;}
	EqMap_aptr eq_map() const {return eq_map_;}
private:

	VarMap_aptr var_map_;
	EqMap_aptr eq_map_;
};

class Problem {
    friend class Constraint_Handle;
    friend class NewMatrixBuilder; // remove deleted lines in _inequs
    friend class Conjunct; // Conjunt::merge_conjs(...)
    
    friend class PrettyPrintVisitor; // _cnts_type
public:
    
    typedef pair<PIntList_aptr, size_t> Ptr2Eq;
//    typedef multimap<size_t, size_t, std::less<size_t> > RowHash;
    typedef bidirectional_multimap<size_t, size_t>::type RowHash;
    
    typedef RowHash::index<first>::type Row_index;
    typedef RowHash::index<second>::type Hash_index;
    
    Problem();
    Problem(size_t n_AllVars);
    
    //Copy (constructor)
    Problem(const Problem & p);
    const Problem & operator = (const Problem & );
    bool operator == (const Problem & other) const;
    bool operator < (const Problem & other) const;
    
    void EliminateVariable(int);
    void EliminateEquVariable(const size_t&, const size_t&); // eliminates equality
    
    int newEQ();
    int newGEQ();
    int newGE();

    coef_t update_coef(const size_t&, Variable_ID, coef_t);
    coef_t update_const(const size_t&, coef_t); //returns updated value
    
    coef_t get_coef(const size_t&, Variable_ID) const;
    coef_t get_const(const size_t&) const;
    
    bool is_in_constr(const size_t&, Variable_ID) const;
    bool is_valid(size_t ) const;
    
    ~Problem();
    bool check_number_INEQs()const;
    /**
    * Validate trivial constraints.
    * Remove parallel facets.
    * Return pair
    * pair.first : bool
    *   return status. False if inconsistent
    * pair.second :size_t
    *   number of eliminated constraints
    *
    **/
 
    void prn_problem()const {
    #ifdef DEBUG_PROBLEM
    	cout<<"\n_inequs"<<*_inequs;
    	cout<<"\n_const"<<*_const;
    	cout<<"\n_cnts_type"<<*_cnts_type;
   	cout<<"\n normalized: "<<_normalized<<flush;
   	cout<<"\nRows Hash:";
   	const Row_index& row_index= _row_hash.get<first>();
   	for (Row_index::const_iterator  it = row_index.begin(); it != row_index.end(); ++it)
            std::cout<<std::endl<<"["<<it->first<<", "<<it->second<<"]";
        cout<<"end"<<endl<<flush;
    #endif
    }

    // return number of inequalities
    size_t size(){return _cnts_type->size();} 

    const Constraint_Property & get_ineq_type(size_t ) const;
    Constraint_Property & ineq_type(size_t );
    size_t nINEQs()const {
        return _inequs->size1();
    }
    size_t nEQUs()const {
    	size_t count = 
    	std::count_if(_cnts_type->begin(), _cnts_type->end(), 
        boost::bind(std::equal_to<Constraint_Type>(),
            boost::bind(&Constraint_Property::type, _1), TEQ));
    	return count;
    }
    
    size_t var_difficulty(const size_t & var_id) const;
/**
 * return index of the bect variable in current step
 * appliable only for system of inequalities
 * best variable has minimal coefficient of 
 * nubber of negative inequalities multiplied to number of
 * positive inequalities min (n_pos * n_neg)
 * return -1 in case of error. It also means that there is
 * no valid variable to eliminate
 */
    int choice_inq(const Variables &vars) const;
/* 
 * if key == 1 or more return index of the best varaible in current step
 * if keq == 1 return index of eny suiteble equality to eliminate
 */ 
   Pair choice_eq(const Variables &vars, const PIntList_aptr &) const;
   bool can_eliminate(const size_t& line_id, const size_t & var_id) const{
    	return ((*_inequs)(line_id, var_id)!=0);	
    };

    bool has_type(const size_t & line_id, Constraint_Property type)const {
    	return ((*_cnts_type)[line_id] == type);
    }

/**
 * remove_eliminated_equ Rebuilds _conjunct and _cnts_type.
 * Removes marked lines
 * Return number of lines were eliminated 
 */

    size_t remove_eliminated();
    /**
    * Online physical line erasing.
    * Used while eaulities elimination
    */
    void erase_line(size_t line_id);
    void reset_line(const size_t & line_id);
    /**
    * marks and checks slimple inequalities ( like 3>1 )
    * and if satisfiable mark it as TREM
    * return false if inconsistency found
    **/
    bool reset_trivial();
    // assumes that all variables were eliminated in the line_id
    // check constant against it's sign
    bool validate_trivial(const size_t & line_id) const; 
    // return true if the line has no variables. For example: 0>=-5
    bool is_trivial(const size_t & line_id) const;
    /**
    * eliminates parallel facets
    * return number of facets were eliminated
    * return number of eliminated fcets 
    * and status if contradiction was found
    * @param red_only
    * if true 
    * BLACK will be treated as redundant only comparing to BLACK
    * if BLAKC implies BLACK - the redundant BLACK will be deleted
    * if BLACK implies RED - the redundant RED will be deleted
    * if RED implies BLACK - nothing
    * if RED implies RED - the redundant RED will be deleted
    * if we could delete BLACK or RED - red will be deleted
    */
    
    RedundantPOut eliminate_p_redundant(Conjunct_ptr, bool red_only = false);
    
    int choice_equ_inequ(const int & eq_no, const coef_t &eq_val, const coef_t &inq_val, const Constraint_Type & inq_type) const;
    RedundantPOut eliminate_p_same(Conjunct_ptr, bool red_only = false);
    RedundantPOut eliminate_p_opposite(Conjunct_ptr, bool red_only = false);
    

    int choice_redundant(const size_t & line_id0, const size_t & line_id1 ) const; //return 0 or 1
    // TODO: refactor and delete it
    int choice_redundant_opposite(const size_t & line_id0, const size_t & line_id1 ) const ;
    
    int normalize_by_var(size_t var_id, Marker & nm);
    int normalize_problem(const Variables & locals);
    
    /// Perform all work needed to change type of constaraint at the line
    
    void change_line_type(size_t line_id, Constraint_Type new_type);
    Ptr2Eq create_ptr2equs()const;
    
	template <class MX, class V> 
	bool export_eq(MX & mx, V & c, EqMapingData & md) const ;
	template <class V>
	bool import_eq(const V & c, const EqMapingData & md);
	bool solve_eqs();
    
private:
    
    SparseMatrix_aptr BuildProjective(size_t);
    void RebuildHash();
    bool HashRemoveRow(const size_t& line_id);
    bool HashRehashRow(size_t  line_id);
    std::pair<bool, size_t> find_opposite_row(size_t ) const;
    
    /// class data
private:
    bool _normalized;
    SparseMatrix_aptr _inequs; /// Matrix each row is an constraint
    
    Constants_aptr _const;  /// the constraint's constants
    
    ConstraintsType_aptr _cnts_type;  //Vector of Constraint types. Index corresponds to row of the _equs matrix

    size_t n_AllVars; //number of ALL variables in the Relation
    		      // map: <hash, matrix_row>
    RowHash _row_hash;

};
typedef Problem * Problem_ptr;
typedef boost::shared_ptr<Problem> Problem_aptr;

class Marker{
    size_t _count;
    PInts _vnorm;
public:
    Marker(size_t);
    bool IsAllMarked() const;
    void Reset(size_t);
    void Mark(size_t index, size_t val);
    bool IsMarked(size_t) const;
    const size_t & operator()(size_t) const;
};
/**
This table is used for simplifying of two constraint
with the same left and right parts but different 
sign. For example (0)x>a & x>=a (1)
table[>][>=] = 1 it means (1) x>a will be deleted
		 1 means (1) ---//---
		-1 means both. Offen it means inconsistency but it's not handled here

=     >  >= REM 0
=   { 1, -1, 0, 0}, 
>   {-1,  1, 0, 0},
>=  { 1,  1, 1, 0},
REM { 1,  1, 1, 1},
1
When we don't care, both could be redundant, it means -1.
**/
enum {DONT_CARE=2, NOT_REDUNDANT=-1, FIRST=0, SECOND=1, INCONS=4, DK2EQU=3, BOTH=7  };
/**
 * Deciding redundant when x (>)(=) a x (>)(=) a and a == b
 **/
static const int redundant_tbl[NUMBER_OF_CONSTRAINT_TYPES][NUMBER_OF_CONSTRAINT_TYPES] = { 
    // = 		>		>=		FIRST
    {DONT_CARE,		INCONS,		FIRST,		NOT_REDUNDANT}, // =
    {INCONS,		DONT_CARE,		FIRST,		NOT_REDUNDANT}, // >
    {SECOND,		SECOND,			DONT_CARE,	NOT_REDUNDANT}, // >=
    {NOT_REDUNDANT,	NOT_REDUNDANT,		NOT_REDUNDANT,	NOT_REDUNDANT}, // SECOND

};
/**
 * Deciding redundant when x (>)(=) a -x (>)(=) b and a == -b
 **/
static const int opposite_redundant_tbl[NUMBER_OF_CONSTRAINT_TYPES][NUMBER_OF_CONSTRAINT_TYPES] = { 
    // = 		>		>=		FIRST
    {DONT_CARE,		INCONS,		FIRST,		NOT_REDUNDANT}, // =
    {INCONS,		INCONS,		INCONS,		NOT_REDUNDANT}, // >
    {SECOND,		INCONS,		DK2EQU,		NOT_REDUNDANT}, // >=
    {NOT_REDUNDANT,	NOT_REDUNDANT,	NOT_REDUNDANT,	NOT_REDUNDANT}, // SECOND

};

};
#endif
